the_w:World, l:IdLnk, mss:Msg List. onlnk(l;mss)  Msg List 

latex

Definitions	World, Msg, onlnk(l;mss), w.M, filter(P;l), a = b, mlnk(m), Msg(M), x:A. B(x), t  T, IdLnk
Lemmas	IdLnk wf, Msg wf, mlnk wf, eq lnk wf, filter wf, world wf